/*
 * LPSolver.hpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef LPSOLVER_HPP_
#define LPSOLVER_HPP_

#include <cassert>

#include <utility>
#include <vector>

#include <lp_lib.h>

#include "bfr/ClauseSet.hpp"
#include "bfr/WinderMatrix.hpp"
#include "bfr/LPB.hpp"
#include "bfr/LPBConversionException.hpp"
#include "bfr/DNFToLPB.hpp"
#include "bfr/BooleanVector.hpp"
#include "bfr/lpbLP/DNFTree.hpp"

namespace bfr {

/**
 * This class is a converter from DNFs to LPBs that uses a
 * Linear Programming algorithm.
 *
 * See <i>Polynomial-time algorithms for regular set-covering
 * and threshold synthesis</i> by Uri N. Peled and Bruno Simeone
 * for the algorithm.
 *
 */
class LPSolver : public DNFToLPB {

    public:
        // TODO: correct?
        // we compare it according a > order, right?
        // TODO doc me
        struct CompareMatrixEntryGe :
            public std::binary_function<const size_t*,
                                        const size_t*,
                                        bool> {
                private:
                    const size_t size;
                public:
                    CompareMatrixEntryGe(size_t s)
                        : size(s) { }
                    bool operator() (const size_t *row1,
                                     const size_t *row2) const {
                        for (size_t i = 0; i < size; i++) {
                            size_t val1 = row1[i];
                            size_t val2 = row2[i];
                            if (val1 == val2)
                                continue;
                            else if (val1 < val2) {
                                return false;
                            }
                            else {
                                return true;
                            }
                        }
                        return false;
                    }
            };

    // TODO don't remember why we have two compare structs
    struct CompareMatrixEntry
        : public std::binary_function<const size_t*, const size_t*, short> {
            private:
                const size_t size;
            public:
                CompareMatrixEntry(size_t s)
                    : size(s) { }

                bool operator() (const size_t *row1,
                                 const size_t *row2) const {
                    for (size_t i = 0; i < size; i++) {
                        size_t val1 = row1[i];
                        size_t val2 = row2[i];
                        if (val1 == val2)
                            continue;
                        else if (val1 < val2) {
                            return -1;
                        }
                        else {
                            return 1;
                        }
                    }
                    return 0;
                }
        };

    struct ComparePoints
    : public std::binary_function<const BooleanVector*,
                                  const BooleanVector*,
                                  bool> {
          public:
        bool operator() (const BooleanVector *p1,
                const BooleanVector *p2) const {
            assert (p1->size() == p2->size());
            size_t size = p1->size();
            bool val1, val2;
            for (size_t i = 0; i < size; i++) {
                val1 = p1->operator [](i);
                val2 = p2->operator [](i);
                if ((!val1) && val2) {
                    return true;
                }
                else if (val1 && (!val2)) {
                    return false;
                }
            }
            assert (false);
            return false;
        }
    };

    /**
     * This enum defines all possible modes to <i>tighten</i> the
     * linear program.
     *
     * See wiki for further information.
     */
    // TODO link me
    enum tighten_lp {
        NONE, /*!< Adds only the constraints that are necessary.*/
        NEIGHBOURS, /*!< Adds also constraints between variables
                         x<sub>i</sub> and x<sub>i + 1</sub>.*/
        ALL /*!< Adds constraint between all variables pairs. */
    };

    /**
     * Constructor.
     *
     * Construct a new solver and set some parameters for it.
     *
     * @param setIntModel If this is set to <code>true</code>,
     * <code>lp_solve</code> is forced to search for an integer
     * solution (what makes the problem much harder).
     * Note that even if you set this value to <code>true</code>
     * <code>lp_solve</code> may still produce solutions that are
     * not integer solutions. It only uses a test on floating point
     * numbers that decides if this float is interpreted as an integer.
     * This test may fail for some float numbers.
     *
     * @param tighten The mode to tighten the LP (number of constraints
     * that will be added, see #bfr::LPSolver::tighten_lp).
     *
     * @param regularityTest The algorithm requires a <i>regularity test</i>.
     * If the test is turned off you may get a wrong result. But if you know
     * that the DNF can be represtented by an LPB you can turn the test off.
     */
    explicit LPSolver(bool setIntModel=false,
            tighten_lp tighten=tighten_lp::NONE, bool regularityTest=true);

    /**
     * Destructor.
     */
    ~LPSolver();

    /**
     * Converts the DNF to an LPB if possible.
     *
     * This will do the following steps:
     *
     * <ol>
     *  <li>Create the #bfr::WinderMatrix</li>
     *  <li>Sort the matrix</li>
     *  <li>Create the list of all <i>minimal true points</i></li>
     *  <li>If regularity test is turned on perform the test</li>
     *  <li>Compute the <i>maximal false</i></li>
     *  <li>Create the LP</li>
     *  <li>Solve the LP</li>
     * </ol>
     * There is a subroutine for nearly all steps in this class.
     *
     * @return An LPB representing the DNF if possible.
     */
    LPB *convert(const ClauseSet* dnf) const throw (LPBConversionException);

    /**
     * Performs the regularity Test.
     *
     * This method will create the #bfr::DNFTree and then run through
     * it as described in
     * <i>Boolean Functions: Theory, Algorithms, and Applications</i>
     * by Yves Crama and Peter L. Hammer.
     *
     * @param dnf The DNF to perform the test on.
     * @param matrix The Winder matrix of the DNF.
     * @param mtps All minimal true points of the DNF.
     */
    bool isRegular(const DNFTree::content_t *dnf, const WinderMatrix &matrix,
            const std::vector<BooleanVector* > &mtps) const;

    /**
     * Sort the matrix according an "importance relation".
     *
     * <b>Note:</b> This method uses <code>std::sort</code>.
     * However I read in
     * <i>Boolean Functions: Theory, Algorithms, and Applications</i>
     * by Yves Crama and Peter L. Hammer that the runtime can be improved
     * in this case.
     *
     * @param matrix The matrix to sort.
     */
    static void sortMatrix(WinderMatrix &matrix);

    // TODO doc me
    static void splitAway(const DNFTree::content_t *dnf, size_t variableID,
            std::pair<const DNFTree::content_t*,
            const DNFTree::content_t*> &result,
            bool *isFirstFinal, bool *isSecondFinal);

    /**
     * Computes the maximal false points.
     *
     * Computes the <i>maximal false points</i> of a DNF given
     * the list of <i>minimal true points</i>.
     *
     * @param mtps The minimal true points of a DNF.
     * @param result The vector that is used to store the
     * maximal false points.
     */
    static void computeMFPs(std::vector<BooleanVector *> &mtps,
            std::vector<BooleanVector *> &result);

    /**
     * Create the linear program.
     *
     * This method will create the linear program that then can
     * be solved with <code>lp_solve</code>.
     *
     * Options of the linear program depend on the parameters of this
     * method.
     *
     * It will always add all necessary constraints.
     *
     * @param mtps The list of <i>minimal true points</i>.
     * @param mfps The list of <i>maximal false points</i>.
     * @param wm The Winder matrix of the DNF.
     * @param intModel If set to <code>true</code> the solution
     * should be an integer solution, however see the remark
     * on the wiki.
     * @param tighten The tighten mode, see #bfr::LPSolver::tighten_lp.
     *
     * @return The linear program that must be solved to compute a solution.
     */
    static lprec *setupLP(const std::vector<BooleanVector *> &mtps,
            const std::vector<BooleanVector *> &mfps,
            const WinderMatrix &wm,
            bool intModel,
            tighten_lp tighten) throw (LPBConversionException);

    /**
     * Solves the linear program.
     *
     * Solves the linear program that has been created before.
     *
     * @param lp The linear program to solve.
     * @param matrix The original winder matrix (required for the right
     * positions of the variables extracted from the LP).
     *
     * @return An LPB representing the DNF the LP was created for.
     */
    static LPB *solveLP(lprec *lp, const WinderMatrix &matrix)
        throw (LPBConversionException);

    private:
    /**
     * Perform an implicant test as described in the Crama / Hammer book.
     */
    bool isImplicant(const DNFTree &tree,
            const BooleanVector *mtp,
            const WinderMatrix &matrix) const;
    bool intModel;
    tighten_lp tighten;
    bool regularityTest;

};

} // namespace bfr


#endif  // LPSOLVER_HPP_
